Failed to solve the following constraints:
  _14 := λ .x → refl [blocked on problem 18]
  [18, 21] _10 _ = f _ : A
Unsolved metas at the following locations:
  Issue483b.agda:12,16-17
  Issue483b.agda:14,10-14
